a, b:kz:KndId fp Top, z:Id.
(z  update-spec-vars(a  b))  (z  update-spec-vars(a))  (z  update-spec-vars(b)) 

latex

Definitions	t  T, x.A(x), x:A. B(x), x. t(x), 2of(t), s = t, Prop, (x  l), P & Q, x:A. B(x), f(a), map(f;as), left+right, P  Q, x:AB(x), P  Q, P  Q, P  Q, Top, update-spec-vars(upd), a  b, a:A fp B(a), IdDeq, KindDeq, Id, Knd, product-deq(A;B;a;b), f  g, x:AB(x), Type, A & B, fpf-domain(f), {T}
Lemmas	fpf-domain-join, fpf wf, fpf-domain wf, fpf-join wf, top wf, product-deq wf, Kind-deq wf, id-deq wf, iff functionality wrt iff, or functionality wrt iff, member map, map wf, l member wf, pi2 wf, Knd wf, Id wf